Recent advances in natural language processing (NLP), particularly large language models (LLMs), have motivated the automatic translation of natural language statements into formal logic without human intervention. This enables automated reasoning and facilitates debugging, finding loop invariants, and adhering to specifications in software systems. However, hallucinations-incorrect outputs generated by LLMs are challenging, particularly for logical translation tasks requiring precision. This work introduces a novel framework that inputs English sentences, converts them into logical expressions, and then translates them into Conjunctive Normal Form (CNF) for satisfiability solving. It employs classical NLP techniques with self-defined grammar, symbolic computation libraries, and a fine-tuned language model to reduce hallucinations. In the early experiments, we observed that the fine-tuned model, trained on different grammar settings, could intentionally correct the same types of hallucinations made by the original model. Thus, it provides reliable CNF generation.

We describe an approach to parsing and logical translation that was inspired by Gazdar's work on context-free grammar for English. Each grammar rule consists of a syntactic part that specifies an acceptable fragment of a parse tree, and a semantic part that specifies how the logical formulas corresponding to the constituents of the fragment are to be combined to yield the formula for the fragment. However, we have sought to reformulate Gazdar's semantic rules so as to obtain more or less'conventional' logical translations of English sentences, avoiding the interpretation of NPs as property sets and the use of intensional functors other than certain propositional operators. The reformulated semantic rules often turn out to be slightly simpler than Gazdar's. Moreover, by using a semantically ambiguous logical syntax for the preliminary translations, we can account for quantifier and coordinator scope ambiguities in syntactically unambiguous sentences without recourse to multiple semantic rules, and are able to separate the disambiguation process from the operation of the parser-translator.